1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro
  5  
  6  Outer measures -- overapproximations of measures
  7  -/
  8  
  9  import algebra.big_operators algebra.module
src         └───────────────────┘ └────────────┘
 10         topology.instances.ennreal analysis.specific_limits
src         └────────────────────────┘ └──────────────────────┘
 11         measure_theory.measurable_space
src         └─────────────────────────────┘
 12  
 13  noncomputable theory
 14  
 15  open set lattice finset function filter encodable
 16  open_locale classical
 17  
 18  namespace measure_theory
 19  
 20  structure outer_measure (α : Type*) :=
 21  (measure_of : set α → ennreal)
 22  (empty : measure_of ∅ = 0)
 23  (mono : ∀{s₁ s₂}, s₁ ⊆ s₂ → measure_of s₁ ≤ measure_of s₂)
 24  (Union_nat : ∀(s:ℕ → set α), measure_of (⋃i, s i) ≤ (∑i, measure_of (s i)))
 25  
 26  namespace outer_measure
 27  
 28  instance {α} : has_coe_to_fun (outer_measure α) := ⟨_, λ m, m.measure_of⟩
id                  └────────────┘  └───────────┘              └─────────┘
src                 └────────────┘  └───────────┘                 └─────────┘
typ                 └────────────┘  └───────────┘              └─────────┘
 29  
 30  section basic
 31  variables {α : Type*} {ms : set (outer_measure α)} {m : outer_measure α}
id                               └─┘  └───────────┘          └───────────┘
src                              └─┘  └───────────┘          └───────────┘
typ                              └─┘  └───────────┘          └───────────┘
 32  
 33  @[simp] theorem empty' (m : outer_measure α) : m ∅ = 0 := m.empty
id                               └───────────┘             └────┘
src                              └───────────┘                └────┘
typ                              └───────────┘             └────┘
doc    └──┘
 34  
 35  theorem mono' (m : outer_measure α) {s₁ s₂}
id                      └───────────┘ 
src                     └───────────┘
typ                     └───────────┘ 
 36    (h : s₁ ⊆ s₂) : m s₁ ≤ m s₂ := m.mono h
id          └┘  └┘     └┘   └┘    └───┘ 
src                                  └───┘
typ         └┘  └┘     └┘   └┘    └───┘ 
 37  
 38  theorem Union_aux (m : set α → ennreal) (m0 : m ∅ = 0)
id                          └─┘    └─────┘          
src                         └─┘     └─────┘           
typ                         └─┘    └─────┘          
doc                                 └─────┘
 39    {β} [encodable β] (s : β → set α) :
id          └───────┘           └─┘ 
src         └───────┘             └─┘
typ         └───────┘           └─┘ 
doc         └───────┘
 40    (∑ b, m (s b)) = ∑ i, m (⋃ b ∈ decode2 β i, s b) :=
id                       └─────┘    
src                             └─────┘    
typ                      └─────┘    
doc                                         
 41  begin
 42    have H : ∀ n, m (⋃ b ∈ decode2 β n, s b) ≠ 0 → (decode2 β n).is_some,
src    └───────┘ └┘    └───┘            └┘ └─┘           └───────┘
typ    └───────┘ └┘    └───┘            └┘ └─┘           └───────┘
doc    └───────┘ └┘    └───┘            └┘ └─┘           └───────┘
txt    └───────┘ └┘    └───┘            └┘ └─┘           └───────┘
par    └───────┘ └┘    └───┘            └┘ └─┘           └───────┘
pid    └────┘└─┘ └┘    └───┘            └┘ └─┘           └──────┘
 43    { intros n h,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
 44      cases decode2 β n with b,
src      └────┘         └─────┘
typ      └────┘         └─────┘
doc      └────┘         └─────┘
txt      └────┘         └─────┘
par      └────┘         └─────┘
pid                    └─────┘
 45      { exact (h (by simp [m0])).elim },
src        └────┘     └────┘  └──────┘
typ        └────┘     └────┘  └──────┘
doc        └────┘     └────┘  └──────┘
txt        └────┘     └────┘  └──────┘
par        └────┘     └────┘  └──────┘
pid                  └─────┘  └─────┘└┘
 46      { exact rfl } },
id               └─┘
src        └────┘└─┘
typ        └────┘└─┘
doc        └────┘   
txt        └────┘   
par        └────┘   
pid                
st     └────────────┘└──┘
 47    refine tsum_eq_tsum_of_ne_zero_bij (λ n h, option.get (H n h)) _ _ _,
id            └─────────────────────────┘         └────────┘  
src    └─────┘└─────────────────────────┘  └────┘└────────┘    └──────┘
typ    └─────┘└─────────────────────────┘  └────┘└────────┘   └──────┘
doc    └─────┘                             └────┘              └──────┘
txt    └─────┘                             └────┘              └──────┘
par    └─────┘                             └────┘              └──────┘
pid                                       └────┘              └──────┘
st   ─────────────────────────────────────────────────────────────────────┘└─
 48    { intros m n hm hn e,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid            └──────────┘
st   ───┘└────────────────┘└─
 49      have := mem_decode2.1 (option.get_mem (H n hn)),
id               └─────────┘    └────────────┘    └┘
src      └──────┘└─────────┘└─┘ └────────────┘     └┘
typ      └──────┘└─────────┘└─┘ └────────────┘ └┘└┘
doc      └──────┘           └─┘                    └┘
txt      └──────┘           └─┘                    └┘
par      └──────┘           └─┘                    └┘
pid      └───┘└─┘           └─┘                    └┘
st   ──────────────────────────────────────────────────┘└─
 50      rwa [← e, mem_decode2.1 (option.get_mem (H m hm))] at this },
id                └─────────┘    └────────────┘    └┘
src      └─────┘ └┘└─────────┘└─┘ └────────────┘     └──────────┘
typ      └─────┘└┘└─────────┘└─┘ └────────────┘ └┘└──────────┘
doc      └─────┘ └┘           └─┘                    └──────────┘
txt      └─────┘ └┘           └─┘                    └──────────┘
par      └─────┘ └┘           └─┘                    └──────────┘
pid         └──┘ └┘           └─┘                    └─┘└──────┘
st   ───────────┘└───────────────────────────────────────┘└───────┘└┘
 51    { intros b h,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ───┘└────────┘└─
 52      refine ⟨encode b, _, _⟩,
id               └────┘ 
src      └─────┘ └────┘ └─────┘
typ      └─────┘ └────┘└─────┘
doc      └─────┘        └─────┘
txt      └─────┘        └─────┘
par      └─────┘        └─────┘
pid                    └─────┘
st   ──────────────────────────┘└─
 53      { convert h, simp [ext_iff, encodek2] },
id                         └─────┘  └──────┘
src        └──────┘   └────┘└─────┘└┘└──────┘└┘
typ        └──────┘  └────┘└─────┘└┘└──────┘└┘
doc        └──────┘   └────┘       └┘        └┘
txt        └──────┘   └────┘       └┘        └┘
par        └──────┘   └────┘       └┘        └┘
pid                             └┘        
st   ─────┘└───────┘└─────────────────────────┘└┘
 54      { exact option.get_of_mem _ (encodek2 _) } },
id               └───────────────┘    └──────┘
src        └────┘└───────────────┘└─┘ └──────┘└──┘
typ        └────┘└───────────────┘└─┘ └──────┘└──┘
doc        └────┘                 └─┘         └──┘
txt        └────┘                 └─┘         └──┘
par        └────┘                 └─┘         └──┘
pid                              └─┘         └─┘
st   ────────────────────────────────────────────┘└──┘
 55    { intros n h,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
 56      transitivity, swap,
src      └──────────┘  └──┘
typ      └──────────┘  └──┘
doc      └──────────┘  └──┘
txt      └──────────┘  └──┘
par      └──────────┘  └──┘
st   ───────────────┘└────┘└─
 57      rw [show decode2 β n = _, from option.get_mem (H n h)],
id                └─────┘             └────────────┘    
src      └──┘    └─────┘  └───────┘└────────────┘    └┘
typ      └──┘    └─────┘ └───────┘└────────────┘ └┘
doc      └──┘              └───────┘                  └┘
txt      └──┘              └───────┘                  └┘
par      └──┘              └───────┘                  └┘
pid        └┘              └───────┘                  └┘
st   ────────────────────────────────────────────────────────┘└──
 58      congr, simp [ext_iff, -option.some_get] }
id                    └─────┘
src      └───┘  └────┘└─────┘└──────────────────┘
typ      └───┘  └────┘└─────┘└──────────────────┘
doc             └────┘       └──────────────────┘
txt      └───┘  └────┘       └──────────────────┘
par      └───┘  └────┘       └──────────────────┘
pid                        └─────────────────┘
st   ────────┘└─────────────────────────────────┘└─
 59  end
st   ──┘
 60  
 61  protected theorem Union (m : outer_measure α)
id                                └───────────┘ 
src                               └───────────┘
typ                               └───────────┘ 
 62    {β} [encodable β] (s : β → set α) :
id          └───────┘           └─┘ 
src         └───────┘             └─┘
typ         └───────┘           └─┘ 
doc         └───────┘
 63    m (⋃i, s i) ≤ (∑i, m (s i)) :=
id                 
src                 
typ                
doc                  
 64  by rw [Union_decode2, Union_aux _ m.empty' s]; exact m.Union_nat _
id          └───────────┘  └───────┘   └──────┘          └─────────┘
src     └──┘└───────────┘└┘└───────┘└─┘└──────┘   └────┘└─────────┘└──
typ     └──┘└───────────┘└┘└───────┘└─┘└──────┘  └────┘└─────────┘└──
doc     └──┘             └┘         └─┘           └────┘           └──
txt     └──┘             └┘         └─┘           └────┘           └──
par     └──┘             └┘         └─┘           └────┘           └──
pid       └┘             └┘         └─┘                           └┘
st     └────────────────┘└──────────────────────┘└─────────────────────
 65  
src  
typ  
doc  
txt  
par  
pid  
st   
 66  lemma Union_null (m : outer_measure α)
id                         └───────────┘ 
src                        └───────────┘
typ                        └───────────┘ 
 67    {β} [encodable β] {s : β → set α} (h : ∀ i, m (s i) = 0) : m (⋃i, s i) = 0 :=
id          └───────┘           └─┘                             
src         └───────┘             └─┘                                      
typ         └───────┘           └─┘                             
doc         └───────┘                                                 
 68  by simpa [h] using m.Union s
id                     └─────┘ 
src     └─────┘ └──────┘└─────┘ 
typ     └─────┘└──────┘└─────┘
doc     └─────┘ └──────┘        
txt     └─────┘ └──────┘        
par     └─────┘ └──────┘        
pid           └────┘        
st     └──────────────────────────
 69  
src  
typ  
doc  
txt  
par  
pid  
st   
 70  protected lemma union (m : outer_measure α) (s₁ s₂ : set α) :
id                              └───────────┘            └─┘ 
src                             └───────────┘             └─┘
typ                             └───────────┘            └─┘ 
 71    m (s₁ ∪ s₂) ≤ m s₁ + m s₂ :=
id       └┘  └┘    └┘   └┘
src                     
typ      └┘  └┘    └┘   └┘
 72  begin
st   └─────
 73    convert m.Union (λ b, cond b s₁ s₂),
id             └─────┘       └──┘   └┘ └┘
src    └──────┘└─────┘  └──┘└──┘     
typ    └──────┘└─────┘  └──┘└──┘ └┘└┘
doc    └──────┘         └──┘         
txt    └──────┘         └──┘         
par    └──────┘         └──┘         
pid                    └──┘         
st   ────────────────────────────────────┘└─
 74    { simp [union_eq_Union] },
id             └────────────┘
src      └────┘└────────────┘└┘
typ      └────┘└────────────┘└┘
doc      └────┘              └┘
txt      └────┘              └┘
par      └────┘              └┘
pid                        
st   ───┘└────────────────────┘└┘
 75    { rw tsum_fintype, change _ = _ + _, simp }
id          └──────────┘              
src      └─┘└──────────┘  └───────┘└─┘└┘  └───┘
typ      └─┘└──────────┘  └───────┘└─┘└┘  └───┘
doc      └─┘              └───────┘ └─┘ └┘  └───┘
txt      └─┘              └───────┘ └─┘ └┘  └───┘
par      └─┘              └───────┘ └─┘ └┘  └───┘
pid                            └─┘ └─┘ └┘      
st   ──────────────────┘└────────────────┘└─────┘└─
 76  end
st   ──┘
 77  
 78  lemma union_null (m : outer_measure α) {s₁ s₂ : set α}
id                         └───────────┘            └─┘ 
src                        └───────────┘             └─┘
typ                        └───────────┘            └─┘ 
 79    (h₁ : m s₁ = 0) (h₂ : m s₂ = 0) : m (s₁ ∪ s₂) = 0 :=
id            └┘            └┘         └┘  └┘  
src                                               
typ           └┘            └┘         └┘  └┘  
 80  by simpa [h₁, h₂] using m.union s₁ s₂
id             └┘  └┘        └─────┘ └┘ └┘
src     └─────┘  └┘  └──────┘└─────┘    
typ     └─────┘└┘└┘└┘└──────┘└─────┘└┘└┘
doc     └─────┘  └┘  └──────┘           
txt     └─────┘  └┘  └──────┘           
par     └─────┘  └┘  └──────┘           
pid            └┘  └────┘           
st     └───────────────────────────────────
 81  
src  
typ  
doc  
txt  
par  
pid  
st   
 82  @[ext] lemma ext : ∀{μ₁ μ₂ : outer_measure α},
id                               └───────────┘ 
src                               └───────────┘
typ                              └───────────┘ 
doc    └─┘
 83    (∀s, μ₁ s = μ₂ s) → μ₁ = μ₂
id         └┘   └┘     └┘  └┘
src                          
typ        └┘   └┘     └┘  └┘
 84  | ⟨m₁, e₁, _, u₁⟩ ⟨m₂, e₂, _, u₂⟩ h := by congr; exact funext h
id                                                          └────┘ 
src                                            └───┘  └────┘└────┘ 
typ                                            └───┘  └────┘└────┘
doc                                                   └────┘       
txt                                            └───┘  └────┘       
par                                            └───┘  └────┘       
pid                                                               
st                                            └──────────────────────
 85  
src  
typ  
doc  
txt  
par  
pid  
st   
 86  instance : has_zero (outer_measure α) :=
id              └──────┘  └───────────┘ 
src             └──────┘  └───────────┘
typ             └──────┘  └───────────┘ 
 87  ⟨{ measure_of := λ_, 0,
id                     
typ                    
 88     empty      := rfl,
id                    └─┘
src                   └─┘
typ                   └─┘
 89     mono       := assume _ _ _, le_refl 0,
id                               └─────┘
src                                 └─────┘
typ                              └─────┘
 90     Union_nat  := assume s, zero_le _ }⟩
id                             └─────┘
src                             └─────┘
typ                            └─────┘
 91  
 92  @[simp] theorem zero_apply (s : set α) : (0 : outer_measure α) s = 0 := rfl
id                                   └─┘          └───────────┘          └─┘
src                                  └─┘           └───────────┘            └─┘
typ                                  └─┘          └───────────┘          └─┘
doc    └──┘
 93  
 94  instance : inhabited (outer_measure α) := ⟨0⟩
id              └───────┘  └───────────┘ 
src             └───────┘  └───────────┘
typ             └───────┘  └───────────┘ 
 95  
 96  instance : has_add (outer_measure α) :=
id              └─────┘  └───────────┘ 
src             └─────┘  └───────────┘
typ             └─────┘  └───────────┘ 
 97  ⟨λm₁ m₂,
id     └┘ └┘
typ    └┘ └┘
 98    { measure_of := λs, m₁ s + m₂ s,
id                        └┘   └┘ 
src                             
typ                       └┘   └┘ 
 99      empty      := show m₁ ∅ + m₂ ∅ = 0, by simp [outer_measure.empty],
id                          └┘   └┘               └─────────────────┘
src                                         └────┘└─────────────────┘
typ                         └┘   └┘         └────┘└─────────────────┘
doc                                             └────┘                   
txt                                             └────┘                   
par                                             └────┘                   
pid                                                                    
st                                             └─────────────────────────┘
100      mono       := assume s₁ s₂ h, add_le_add' (m₁.mono h) (m₂.mono h),
id                            └┘ └┘   └─────────┘  └┘└───┘    └┘└───┘ 
src                                    └─────────┘    └───┘       └───┘
typ                           └┘ └┘   └─────────┘  └┘└───┘    └┘└───┘ 
101      Union_nat  := assume s,
id                            
typ                           
102        calc m₁ (⋃i, s i) + m₂ (⋃i, s i) ≤
id              └┘       └┘    
src                              
typ             └┘       └┘    
doc                               
103            (∑i, m₁ (s i)) + (∑i, m₂ (s i)) :
id               └┘         └┘   
src                            
typ              └┘         └┘   
doc                             
104            add_le_add' (m₁.Union_nat s) (m₂.Union_nat s)
id             └─────────┘  └┘└────────┘    └┘└────────┘ 
src            └─────────┘    └────────┘       └────────┘
typ            └─────────┘  └┘└────────┘    └┘└────────┘ 
105          ... = _ : ennreal.tsum_add.symm}⟩
id                     └──────────────┘└───┘
src                    └──────────────┘└───┘
typ                    └──────────────┘└───┘
st                  
106  
107  @[simp] theorem add_apply (m₁ m₂ : outer_measure α) (s : set α) :
id                                      └───────────┘        └─┘ 
src                                     └───────────┘         └─┘
typ                                     └───────────┘        └─┘ 
doc    └──┘
108    (m₁ + m₂) s = m₁ s + m₂ s := rfl
id      └┘  └┘    └┘   └┘     └─┘
src                              └─┘
typ     └┘  └┘    └┘   └┘     └─┘
109  
110  instance add_comm_monoid : add_comm_monoid (outer_measure α) :=
id                              └─────────────┘  └───────────┘ 
src                             └─────────────┘  └───────────┘
typ                             └─────────────┘  └───────────┘ 
111  { zero      := 0,
112    add       := (+),
id                  
src                 
typ                 
113    add_comm  := assume a b, ext $ assume s, add_comm _ _,
id                            └─┘            └──────┘
src                             └─┘             └──────┘
typ                           └─┘            └──────┘
114    add_assoc := assume a b c, ext $ assume s, add_assoc _ _ _,
id                             └─┘            └───────┘
src                               └─┘             └───────┘
typ                            └─┘            └───────┘
115    add_zero  := assume a, ext $ assume s, add_zero _,
id                           └─┘            └──────┘
src                           └─┘             └──────┘
typ                          └─┘            └──────┘
116    zero_add  := assume a, ext $ assume s, zero_add _ }
id                           └─┘            └──────┘
src                           └─┘             └──────┘
typ                          └─┘            └──────┘
117  
118  instance : has_bot (outer_measure α) := ⟨0⟩
id              └─────┘  └───────────┘ 
src             └─────┘  └───────────┘
typ             └─────┘  └───────────┘ 
doc             └─────┘
119  
120  instance outer_measure.order_bot : order_bot (outer_measure α) :=
id                                      └───────┘  └───────────┘ 
src                                     └───────┘  └───────────┘
typ                                     └───────┘  └───────────┘ 
doc                                     └───────┘
121  { le          := λm₁ m₂, ∀s, m₁ s ≤ m₂ s,
id                    └┘ └┘     └┘   └┘ 
src                                   
typ                   └┘ └┘     └┘   └┘ 
122    bot         := 0,
123    le_refl     := assume a s, le_refl _,
id                              └─────┘
src                               └─────┘
typ                             └─────┘
124    le_trans    := assume a b c hab hbc s, le_trans (hab s) (hbc s),
id                              └─┘ └─┘   └──────┘  └─┘    └─┘ 
src                                           └──────┘
typ                             └─┘ └─┘   └──────┘  └─┘    └─┘ 
125    le_antisymm := assume a b hab hba, ext $ assume s, le_antisymm (hab s) (hba s),
id                             └─┘ └─┘  └─┘            └─────────┘  └─┘    └─┘ 
src                                       └─┘             └─────────┘
typ                            └─┘ └─┘  └─┘            └─────────┘  └─┘    └─┘ 
126    bot_le      := assume a s, zero_le _ }
id                              └─────┘
src                               └─────┘
typ                             └─────┘
127  
128  section supremum
129  
130  instance : has_Sup (outer_measure α) :=
id              └─────┘  └───────────┘ 
src             └─────┘  └───────────┘
typ             └─────┘  └───────────┘ 
doc             └─────┘
131  ⟨λms, {
id     └┘
typ    └┘
132    measure_of := λs, ⨆m:ms, m.val s,
id                        └┘ └──┘ 
src                            └──┘
typ                       └┘ └──┘ 
doc                          
133    empty      := le_zero_iff_eq.1 $ supr_le $ λ ⟨m, h⟩, le_of_eq m.empty,
id                   └────────────┘    └─────┘           └──────┘  └────┘
src                  └────────────┘    └─────┘             └──────┘  └────┘
typ                  └────────────┘    └─────┘           └──────┘  └────┘
134    mono       := assume s₁ s₂ hs, supr_le_supr $ assume ⟨m, hm⟩, m.mono hs,
id                          └┘ └┘ └┘  └──────────┘                  └───┘ └┘
src                                   └──────────┘                    └───┘
typ                         └┘ └┘ └┘  └──────────┘                  └───┘ └┘
135    Union_nat  := assume f, supr_le $ assume m,
id                            └─────┘          
src                            └─────┘
typ                           └─────┘          
136      calc m.val (⋃i, f i) ≤ (∑ (i : ℕ), m.val (f i)) : m.val.Union_nat _
id            └──┘                 └──┘        └──┘└────────┘
src            └──┘                     └──┘           └──┘└────────┘
typ           └──┘                 └──┘        └──┘└────────┘
doc                                    
137        ... ≤ (∑i, ⨆m:ms, m.val (f i)) :
id                   └┘ └──┘   
src                       └──┘
typ                  └┘ └──┘   
doc                     
138          ennreal.tsum_le_tsum $ assume i, le_supr (λm:ms, m.val (f i)) m }⟩
id           └──────────────────┘            └─────┘     └┘  └──┘      
src          └──────────────────┘             └─────┘          └──┘
typ          └──────────────────┘            └─────┘     └┘  └──┘      
139  
140  private lemma le_Sup (hm : m ∈ ms) : m ≤ Sup ms :=
id                                └┘      └─┘ └┘
src                                         └─┘
typ                               └┘      └─┘ └┘
doc                                           └─┘
141  λ s, le_supr (λm:ms, m.val s) ⟨m, hm⟩
id       └─────┘     └┘  └──┘      └┘
src       └─────┘          └──┘
typ      └─────┘     └┘  └──┘      └┘
142  
143  private lemma Sup_le (hm : ∀m' ∈ ms, m' ≤ m) : Sup ms ≤ m :=
id                               └┘   └┘  └┘      └─┘ └┘  
src                              └┘                └─┘    
typ                              └┘   └┘  └┘      └─┘ └┘  
doc                                                 └─┘
144  λ s, (supr_le $ assume ⟨m', h'⟩, (hm m' h') s)
id        └─────┘          └┘  └┘    └┘        
src        └─────┘
typ       └─────┘          └┘  └┘    └┘        
145  
146  instance : has_Inf (outer_measure α) := ⟨λs, Sup {m | ∀m'∈s, m ≤ m'}⟩
id              └─────┘  └───────────┘          └─┘     └┘     └┘
src             └─────┘  └───────────┘            └─┘              
typ             └─────┘  └───────────┘          └─┘     └┘     └┘
doc             └─────┘                           └─┘
147  private lemma Inf_le (hm : m ∈ ms) : Inf ms ≤ m := Sup_le $ assume m' h', h' _ hm
id                                └┘    └─┘ └┘      └────┘          └┘ └┘  └┘   └┘
src                                      └─┘          └────┘
typ                               └┘    └─┘ └┘      └────┘          └┘ └┘  └┘   └┘
doc                                       └─┘
148  private lemma le_Inf (hm : ∀m' ∈ ms, m ≤ m') : m ≤ Inf ms := le_Sup hm
id                               └┘   └┘    └┘      └─┘ └┘    └────┘ └┘
src                                                   └─┘       └────┘
typ                              └┘   └┘    └┘      └─┘ └┘    └────┘ └┘
doc                                                     └─┘
149  
150  instance : complete_lattice (outer_measure α) :=
id              └──────────────┘  └───────────┘ 
src             └──────────────┘  └───────────┘
typ             └──────────────┘  └───────────┘ 
doc             └──────────────┘
151  { top          := Sup univ,
id                     └─┘ └──┘
src                    └─┘ └──┘
typ                    └─┘ └──┘
doc                    └─┘
152    le_top       := assume a, le_Sup (mem_univ a),
id                              └────┘  └──────┘ 
src                              └────┘  └──────┘
typ                             └────┘  └──────┘ 
153    Sup          := Sup,
id                     └─┘
src                    └─┘
typ                    └─┘
doc                    └─┘
154    Sup_le       := assume s m, Sup_le,
id                               └────┘
src                                └────┘
typ                              └────┘
155    le_Sup       := assume s m, le_Sup,
id                               └────┘
src                                └────┘
typ                              └────┘
156    Inf          := Inf,
id                     └─┘
src                    └─┘
typ                    └─┘
doc                    └─┘
157    Inf_le       := assume s m, Inf_le,
id                               └────┘
src                                └────┘
typ                              └────┘
158    le_Inf       := assume s m, le_Inf,
id                               └────┘
src                                └────┘
typ                              └────┘
159    sup          := λa b, Sup {a, b},
id                         └─┘  
src                          └─┘  
typ                        └─┘  
doc                          └─┘
160    le_sup_left  := assume a b, le_Sup $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
161    le_sup_right := assume a b, le_Sup $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
162    sup_le       := assume a b c ha hb, Sup_le $ by simp [or_imp_distrib, ha, hb] {contextual:=tt},
id                               └┘ └┘  └────┘            └────────────┘  └┘  └┘               └┘
src                                        └────┘      └────┘└────────────┘└┘  └┘  └┘ └──────────┘└┘
typ                              └┘ └┘  └────┘      └────┘└────────────┘└┘└┘└┘└┘└┘ └──────────┘└┘
doc                                                    └────┘              └┘  └┘  └┘ └──────────┘  
txt                                                    └────┘              └┘  └┘  └┘ └──────────┘  
par                                                    └────┘              └┘  └┘  └┘ └──────────┘  
pid                                                                      └┘  └┘   └──────────┘  
st                                                    └─────────────────────────────────────────────┘
163    inf          := λa b, Inf {a, b},
id                         └─┘  
src                          └─┘  
typ                        └─┘  
doc                          └─┘
164    inf_le_left  := assume a b, Inf_le $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
165    inf_le_right := assume a b, Inf_le $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
166    le_inf       := assume a b c ha hb, le_Inf $ by simp [or_imp_distrib, ha, hb] {contextual:=tt},
id                               └┘ └┘  └────┘            └────────────┘  └┘  └┘               └┘
src                                        └────┘      └────┘└────────────┘└┘  └┘  └┘ └──────────┘└┘
typ                              └┘ └┘  └────┘      └────┘└────────────┘└┘└┘└┘└┘└┘ └──────────┘└┘
doc                                                    └────┘              └┘  └┘  └┘ └──────────┘  
txt                                                    └────┘              └┘  └┘  └┘ └──────────┘  
par                                                    └────┘              └┘  └┘  └┘ └──────────┘  
pid                                                                      └┘  └┘   └──────────┘  
st                                                    └─────────────────────────────────────────────┘
167    .. outer_measure.order_bot }
id        └─────────────────────┘
src       └─────────────────────┘
typ       └─────────────────────┘
168  
169  @[simp] theorem Sup_apply (ms : set (outer_measure α)) (s : set α) :
id                                   └─┘  └───────────┘         └─┘ 
src                                  └─┘  └───────────┘          └─┘
typ                                  └─┘  └───────────┘         └─┘ 
doc    └──┘
170    (Sup ms) s = ⨆ m : ms, m s := rfl
id      └─┘ └┘         └┘      └─┘
src     └─┘                       └─┘
typ     └─┘ └┘         └┘      └─┘
doc     └─┘                
171  
172  @[simp] theorem supr_apply {ι} (f : ι → outer_measure α) (s : set α) :
id                                          └───────────┘        └─┘ 
src                                          └───────────┘         └─┘
typ                                         └───────────┘        └─┘ 
doc    └──┘
173    (⨆ i : ι, f i) s = ⨆ i, f i s :=
id                     
src                      
typ                    
doc                       
174  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
175    (supr_le $ λ ⟨_, i, rfl⟩, le_supr _ i)
id      └─────┘          └─┘   └─────┘
src     └─────┘            └─┘   └─────┘
typ     └─────┘          └─┘   └─────┘
176    (supr_le $ λ i, le_supr
id      └─────┘       └─────┘
src     └─────┘        └─────┘
typ     └─────┘       └─────┘
177      (λ (m : {a : outer_measure α // ∃ i, f i = a}), m.1 s)
id                   └───────────┘                
src                  └───────────┘                    
typ                  └───────────┘                
178      ⟨f i, i, rfl⟩)
id             └─┘
src               └─┘
typ            └─┘
179  
180  @[simp] theorem sup_apply (m₁ m₂ : outer_measure α) (s : set α) :
id                                      └───────────┘        └─┘ 
src                                     └───────────┘         └─┘
typ                                     └───────────┘        └─┘ 
doc    └──┘
181    (m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s :=
id      └┘  └┘    └┘   └┘ 
src                     
typ     └┘  └┘    └┘   └┘ 
182  by have := supr_apply (λ b, cond b m₁ m₂) s;
id              └────────┘       └──┘   └┘ └┘  
src     └──────┘└────────┘  └──┘└──┘     └┘
typ     └──────┘└────────┘  └──┘└──┘ └┘└┘└┘
doc     └──────┘            └──┘         └┘
txt     └──────┘            └──┘         └┘
par     └──────┘            └──┘         └┘
pid     └───┘└─┘            └──┘         └┘
st     └──────────────────────────────────────────
183    rwa [supr_bool_eq, supr_bool_eq] at this
id          └──────────┘  └──────────┘
src    └───┘└──────────┘└┘└──────────┘└─────────
typ    └───┘└──────────┘└┘└──────────┘└─────────
doc    └───┘            └┘            └─────────
txt    └───┘            └┘            └─────────
par    └───┘            └┘            └─────────
pid       └┘            └┘            └──────┘
st   ──────┘└──────────┘└────────────┘└────────
184  
src  
typ  
doc  
txt  
par  
pid  
st   
185  end supremum
186  
187  def map {β} (f : α → β) (m : outer_measure α) : outer_measure β :=
id                              └───────────┘     └───────────┘ 
src                               └───────────┘      └───────────┘
typ                             └───────────┘     └───────────┘ 
188  { measure_of := λs, m (f ⁻¹' s),
id                         └─┘ 
src                           └─┘
typ                        └─┘ 
doc                           └─┘
189    empty := m.empty,
id              └────┘
src              └────┘
typ             └────┘
190    mono := λ s t h, m.mono (preimage_mono h),
id                   └───┘  └───────────┘ 
src                      └───┘  └───────────┘
typ                  └───┘  └───────────┘ 
191    Union_nat := λ s, by rw [preimage_Union]; exact
id                             └────────────┘
src                         └──┘└────────────┘  └─────
typ                        └──┘└────────────┘  └─────
doc                         └──┘                └─────
txt                         └──┘                └─────
par                         └──┘                └─────
pid                           └┘                     
st                         └─────────────────┘└───────
192      m.Union_nat (λ i, f ⁻¹' s i) }
id       └─────────┘        └─┘ 
src  ───┘└─────────┘  └──┘ └─┘  └┘
typ  ───┘└─────────┘  └──┘└─┘ └┘
doc  ───┘             └──┘ └─┘  └┘
txt  ───┘             └──┘      └┘
par  ───┘             └──┘      └┘
pid  ───┘             └──┘      
st   ────────────────────────────────┘
193  
194  @[simp] theorem map_apply {β} (f : α → β)
id                                         
typ                                        
doc    └──┘
195    (m : outer_measure α) (s : set β) : map f m s = m (f ⁻¹' s) := rfl
id          └───────────┘        └─┘     └─┘        └─┘      └─┘
src         └───────────┘         └─┘      └─┘             └─┘       └─┘
typ         └───────────┘        └─┘     └─┘        └─┘      └─┘
doc                                                         └─┘
196  
197  @[simp] theorem map_id (m : outer_measure α) : map id m = m :=
id                               └───────────┘     └─┘ └┘   
src                              └───────────┘      └─┘ └┘   
typ                              └───────────┘     └─┘ └┘   
doc    └──┘
198  ext $ λ s, rfl
id   └─┘       └─┘
src  └─┘        └─┘
typ  └─┘       └─┘
199  
200  @[simp] theorem map_map {β γ} (f : α → β) (g : β → γ)
id                                                   
typ                                                  
doc    └──┘
201    (m : outer_measure α) : map g (map f m) = map (g ∘ f) m :=
id          └───────────┘     └─┘   └─┘     └─┘      
src         └───────────┘      └─┘    └─┘       └─┘    
typ         └───────────┘     └─┘   └─┘     └─┘      
202  ext $ λ s, rfl
id   └─┘       └─┘
src  └─┘        └─┘
typ  └─┘       └─┘
203  
204  instance : functor outer_measure := {map := λ α β, map}
id              └─────┘ └───────────┘                 └─┘
src             └─────┘ └───────────┘                   └─┘
typ             └─────┘ └───────────┘                 └─┘
205  
206  instance : is_lawful_functor outer_measure :=
id              └───────────────┘ └───────────┘
src             └───────────────┘ └───────────┘
typ             └───────────────┘ └───────────┘
207  { id_map := λ α, map_id,
id                  └────┘
src                  └────┘
typ                 └────┘
208    comp_map := λ α β γ f g m, (map_map f g m).symm }
id                           └─────┘    └──┘
src                                └─────┘       └──┘
typ                          └─────┘    └──┘
209  
210  /-- The dirac outer measure. -/
211  def dirac (a : α) : outer_measure α :=
id                      └───────────┘ 
src                      └───────────┘
typ                     └───────────┘ 
212  { measure_of := λs, ⨆ h : a ∈ s, 1,
id                             
src                               
typ                            
doc                                
213    empty := by simp,
src                └──┘
typ                └──┘
doc                └──┘
txt                └──┘
par                └──┘
st                └───┘
214    mono := λ s t h, supr_le_supr2 (λ h', ⟨h h', le_refl _⟩),
id                   └───────────┘    └┘    └┘  └─────┘
src                     └───────────┘               └─────┘
typ                  └───────────┘    └┘    └┘  └─────┘
215    Union_nat := λ s, supr_le $ λ h,
id                      └─────┘     
src                      └─────┘
typ                     └─────┘     
216      let ⟨i, h⟩ := mem_Union.1 h in
id       └─┘          └───────┘  
src                    └───────┘
typ      └─┘          └───────┘  
217      le_trans (by exact le_supr _ h) (ennreal.le_tsum i) }
id       └──────┘           └─────┘      └─────────────┘
src      └──────┘     └────┘└─────┘└─┘    └─────────────┘
typ      └──────┘     └────┘└─────┘└─┘   └─────────────┘
doc                   └────┘       └─┘
txt                   └────┘       └─┘
par                   └────┘       └─┘
pid                               └─┘
st                   └────────────────┘
218  
219  @[simp] theorem dirac_apply (a : α) (s : set α) :
id                                           └─┘ 
src                                           └─┘
typ                                          └─┘ 
doc    └──┘
220    dirac a s = ⨆ h : a ∈ s, 1 := rfl
id     └───┘                 └─┘
src    └───┘                     └─┘
typ    └───┘                 └─┘
doc    └───┘                 
221  
222  def sum {ι} (f : ι → outer_measure α) : outer_measure α :=
id                       └───────────┘     └───────────┘ 
src                       └───────────┘      └───────────┘
typ                      └───────────┘     └───────────┘ 
223  { measure_of := λs, ∑ i, f i s,
id                          
src                        
typ                         
doc                        
224    empty := by simp,
src                └──┘
typ                └──┘
doc                └──┘
txt                └──┘
par                └──┘
st                └───┘
225    mono := λ s t h, ennreal.tsum_le_tsum (λ i, (f i).mono' h),
id                   └──────────────────┘         └───┘  
src                     └──────────────────┘            └───┘
typ                  └──────────────────┘         └───┘  
226    Union_nat := λ s, by rw ennreal.tsum_comm; exact
id                            └───────────────┘
src                         └─┘└───────────────┘  └─────
typ                        └─┘└───────────────┘  └─────
doc                         └─┘                   └─────
txt                         └─┘                   └─────
par                         └─┘                   └─────
pid                                                   
st                         └────────────────────────────
227      ennreal.tsum_le_tsum (λ i, (f i).Union_nat _) }
id       └──────────────────┘        
src  ───┘└──────────────────┘  └──┘   └─────────────┘
typ  ───┘└──────────────────┘  └──┘  └─────────────┘
doc  ───┘                      └──┘   └─────────────┘
txt  ───┘                      └──┘   └─────────────┘
par  ───┘                      └──┘   └─────────────┘
pid  ───┘                      └──┘   └────────────┘
st   ─────────────────────────────────────────────────┘
228  
229  @[simp] theorem sum_apply {ι} (f : ι → outer_measure α) (s : set α) :
id                                         └───────────┘        └─┘ 
src                                         └───────────┘         └─┘
typ                                        └───────────┘        └─┘ 
doc    └──┘
230    sum f s = ∑ i, f i s := rfl
id     └─┘            └─┘
src    └─┘                  └─┘
typ    └─┘            └─┘
doc                
231  
232  instance : has_scalar ennreal (outer_measure α) :=
id              └────────┘ └─────┘  └───────────┘ 
src             └────────┘ └─────┘  └───────────┘
typ             └────────┘ └─────┘  └───────────┘ 
doc             └────────┘ └─────┘
233  ⟨λ a m, {
id       
typ      
234    measure_of := λs, a * m s,
id                         
src                        
typ                        
235    empty := by simp,
src                └──┘
typ                └──┘
doc                └──┘
txt                └──┘
par                └──┘
st                └───┘
236    mono := λ s t h, canonically_ordered_semiring.mul_le_mul (le_refl _) (m.mono' h),
id                   └─────────────────────────────────────┘  └─────┘     └────┘ 
src                     └─────────────────────────────────────┘  └─────┘      └────┘
typ                  └─────────────────────────────────────┘  └─────┘     └────┘ 
237    Union_nat := λ s, by rw ennreal.mul_tsum; exact
id                            └──────────────┘
src                         └─┘└──────────────┘  └─────
typ                        └─┘└──────────────┘  └─────
doc                         └─┘                  └─────
txt                         └─┘                  └─────
par                         └─┘                  └─────
pid                                                  
st                         └───────────────────────────
238      canonically_ordered_semiring.mul_le_mul (le_refl _) (m.Union_nat _) }⟩
id       └─────────────────────────────────────┘  └─────┘     └─────────┘
src  ───┘└─────────────────────────────────────┘ └─────┘└──┘ └─────────┘└──┘
typ  ───┘└─────────────────────────────────────┘ └─────┘└──┘ └─────────┘└──┘
doc  ───┘                                               └──┘            └──┘
txt  ───┘                                               └──┘            └──┘
par  ───┘                                               └──┘            └──┘
pid  ───┘                                               └──┘            └─┘
st   ───────────────────────────────────────────────────────────────────────┘
239  
240  @[simp] theorem smul_apply (a : ennreal) (m : outer_measure α) (s : set α) :
id                                   └─────┘       └───────────┘        └─┘ 
src                                  └─────┘       └───────────┘         └─┘
typ                                  └─────┘       └───────────┘        └─┘ 
doc    └──┘                          └─────┘
241    (a • m) s = a * m s := rfl
id                   └─┘
src                        └─┘
typ                  └─┘
242  
243  instance : semimodule ennreal (outer_measure α) :=
id              └────────┘ └─────┘  └───────────┘ 
src             └────────┘ └─────┘  └───────────┘
typ             └────────┘ └─────┘  └───────────┘ 
doc             └────────┘ └─────┘
244  { smul_add := λ a m₁ m₂, ext $ λ s, mul_add _ _ _,
id                    └┘ └┘  └─┘       └─────┘
src                           └─┘        └─────┘
typ                   └┘ └┘  └─┘       └─────┘
245    add_smul := λ a b m, ext $ λ s, add_mul _ _ _,
id                       └─┘       └─────┘
src                         └─┘        └─────┘
typ                      └─┘       └─────┘
246    mul_smul := λ a b m, ext $ λ s, mul_assoc _ _ _,
id                       └─┘       └───────┘
src                         └─┘        └───────┘
typ                      └─┘       └───────┘
247    one_smul := λ m, ext $ λ s, one_mul _,
id                     └─┘       └─────┘
src                     └─┘        └─────┘
typ                    └─┘       └─────┘
248    zero_smul := λ m, ext $ λ s, zero_mul _,
id                      └─┘       └──────┘
src                      └─┘        └──────┘
typ                     └─┘       └──────┘
249    smul_zero := λ a, ext $ λ s, mul_zero _,
id                      └─┘       └──────┘
src                      └─┘        └──────┘
typ                     └─┘       └──────┘
250    ..outer_measure.has_scalar }
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
251  
252  theorem smul_dirac_apply (a : ennreal) (b : α) (s : set α) :
id                                 └─────┘              └─┘ 
src                                └─────┘               └─┘
typ                                └─────┘              └─┘ 
doc                                └─────┘
253    (a • dirac b) s = ⨆ h : b ∈ s, a :=
id        └───┘             
src        └───┘                
typ       └───┘             
doc         └───┘                  
254  by by_cases b ∈ s; simp [h]
id                         
src     └───────┘    └────┘ └─
typ     └───────┘  └────┘└─
doc     └───────┘     └────┘ └─
txt     └───────┘     └────┘ └─
par     └───────┘     └────┘ └─
pid                       
st     └─────────────────────────
255  
src  
typ  
doc  
txt  
par  
pid  
st   
256  theorem top_apply {s : set α} (h : s.nonempty) : (⊤ : outer_measure α) s = ⊤ :=
id                          └─┘        └───────┘        └───────────┘     
src                         └─┘          └───────┘        └───────────┘       
typ                         └─┘        └───────┘        └───────────┘     
doc                                      └───────┘
257  let ⟨a, as⟩ := h in
id   └─┘           
typ  └─┘           
258  top_unique $ le_supr_of_le ⟨(⊤ : ennreal) • dirac a, trivial⟩ $
id   └────────┘   └───────────┘      └─────┘   └───┘    └─────┘
src  └────────┘   └───────────┘      └─────┘   └───┘    └─────┘
typ  └────────┘   └───────────┘      └─────┘   └───┘    └─────┘
doc                                   └─────┘    └───┘
259  by simp [smul_dirac_apply, as]
id            └──────────────┘  └┘
src     └────┘└──────────────┘└┘  └─
typ     └────┘└──────────────┘└┘└┘└─
doc     └────┘                └┘  └─
txt     └────┘                └┘  └─
par     └────┘                └┘  └─
pid                         └┘  
st     └────────────────────────────
260  
src  
typ  
doc  
txt  
par  
pid  
st   
261  end basic
262  
263  section of_function
264  set_option eqn_compiler.zeta true
doc             └───────────────┘
265  
266  /-- Given any function `m` assigning measures to sets satisying `m ∅ = 0`, there is
267    a unique maximal outer measure `μ` satisfying `μ s ≤ m s` for all `s : set α`. -/
268  protected def of_function {α : Type*} (m : set α → ennreal) (m_empty : m ∅ = 0) :
id                                              └─┘    └─────┘               
src                                             └─┘     └─────┘                
typ                                             └─┘    └─────┘               
doc                                                     └─────┘
269    outer_measure α :=
id     └───────────┘ 
src    └───────────┘
typ    └───────────┘ 
270  let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑i, m (f i) in
id                     └─┘                  
src                       └─┘                    
typ                    └─┘                  
doc                                                
271  { measure_of := μ,
id                   
typ                  
272    empty      := le_antisymm
id                   └─────────┘
src                  └─────────┘
typ                  └─────────┘
273      (infi_le_of_le (λ_, ∅) $ infi_le_of_le (empty_subset _) $ by simp [m_empty])
id        └───────────┘         └───────────┘  └──────────┘               └─────┘
src       └───────────┘          └───────────┘  └──────────┘         └────┘       
typ       └───────────┘         └───────────┘  └──────────┘         └────┘└─────┘
doc                                                                   └────┘       
txt                                                                   └────┘       
par                                                                   └────┘       
pid                                                                              
st                                                                   └─────────────┘
274      (zero_le _),
id        └─────┘
src       └─────┘
typ       └─────┘
275    mono       := assume s₁ s₂ hs, infi_le_infi $ assume f,
id                          └┘ └┘ └┘  └──────────┘          
src                                   └──────────┘
typ                         └┘ └┘ └┘  └──────────┘          
276      infi_le_infi2 $ assume hb, ⟨subset.trans hs hb, le_refl _⟩,
id       └───────────┘          └┘   └──────────┘ └┘ └┘  └─────┘
src      └───────────┘               └──────────┘        └─────┘
typ      └───────────┘          └┘   └──────────┘ └┘ └┘  └─────┘
277    Union_nat := assume s, ennreal.le_of_forall_epsilon_le $ begin
id                           └─────────────────────────────┘
src                           └─────────────────────────────┘
typ                          └─────────────────────────────┘
st                                                              └─────
278      assume ε hε (hb : (∑i, μ (s i)) < ⊤),
id                                    
src      └────────────────┘     └─┘
typ      └────────────────┘   └─┘
doc      └────────────────┘     └─┘  
txt      └────────────────┘       └─┘  
par      └────────────────┘       └─┘  
pid      └────────────────┘       └─┘  
st   ───────────────────────────────────────┘└─
279      rcases ennreal.exists_pos_sum_of_encodable (ennreal.coe_lt_coe.2 hε) ℕ with ⟨ε', hε', hl⟩,
id              └─────────────────────────────────┘  └────────────────┘   └┘
src      └─────┘└─────────────────────────────────┘ └────────────────┘└─┘  └┘ └─────────────────┘
typ      └─────┘└─────────────────────────────────┘ └────────────────┘└─┘└┘└┘ └─────────────────┘
doc      └─────┘                                                      └─┘  └┘ └─────────────────┘
txt      └─────┘                                                      └─┘  └┘ └─────────────────┘
par      └─────┘                                                      └─┘  └┘ └─────────────────┘
pid                                                                  └─┘  └┘ └─────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
280      refine le_trans _ (add_le_add_left' (le_of_lt hl)),
id              └──────┘    └──────────────┘  └──────┘ └┘
src      └─────┘└──────┘└─┘ └──────────────┘ └──────┘  └┘
typ      └─────┘└──────┘└─┘ └──────────────┘ └──────┘└┘└┘
doc      └─────┘        └─┘                            └┘
txt      └─────┘        └─┘                            └┘
par      └─────┘        └─┘                            └┘
pid                    └─┘                            └┘
st   ─────────────────────────────────────────────────────┘└─
281      rw ← ennreal.tsum_add,
id            └──────────────┘
src      └───┘└──────────────┘
typ      └───┘└──────────────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ────────────────────────┘└─
282      choose f hf using show
src      └────────────────┘    
typ      └────────────────┘    
doc      └────────────────┘    
txt      └────────────────┘    
par      └────────────────┘    
pid            └┘└─┘└─────┘    
st   ───────────────────────────
283        ∀i, ∃f:ℕ → set α, s i ⊆ (⋃i, f i) ∧ (∑i, m (f i)) < μ (s i) + ε' i,
id                  └─┘                                     └┘
src  ─────┘  └┘  └─┘      └┘      └─┘     └┘   └─
typ  ─────┘  └┘ └─┘     └┘     └─┘   └┘└┘ └─
doc  ─────┘   └┘             └┘      └─┘     └┘    └─
txt  ─────┘   └┘               └┘        └─┘     └┘    └─
par  ─────┘   └┘               └┘        └─┘     └┘    └─
pid  ─────┘   └┘               └┘        └─┘     └┘    └─
st   ──────────────────────────────────────────────────────────────────────────
284      { intro,
src  ─────┘└───┘└─
typ  ─────┘└───┘└─
doc  ─────┘└───┘└─
txt  ─────┘└───┘└─
par  ─────┘└───┘└─
pid  ─────────────
st   ────┘└────┘└─
285        have : μ (s i) < μ (s i) + ε' i :=
id                                  └┘ 
src  ─────┘└─────┘    └┘     └┘    └───
typ  ─────┘└─────┘    └┘   └┘ └┘└───
doc  ─────┘└─────┘    └┘     └┘    └───
txt  ─────┘└─────┘    └┘     └┘    └───
par  ─────┘└─────┘    └┘     └┘    └───
pid  ────────────┘    └┘     └┘    └───
st   ─────────────────────────────────────────
286          ennreal.lt_add_right
id           └──────────────────┘
src  ───────┘└──────────────────┘
typ  ───────┘└──────────────────┘
doc  ───────┘                    
txt  ───────┘                    
par  ───────┘                    
pid  ───────┘                    
st   ─────────────────────────────
287            (lt_of_le_of_lt (by apply ennreal.le_tsum) hb)
id              └────────────┘           └─────────────┘  └┘
src  ─────────┘ └────────────┘   └────┘└─────────────┘└┘  └─
typ  ─────────┘ └────────────┘   └────┘└─────────────┘└┘└┘└─
doc  ─────────┘                  └────┘               └┘  └─
txt  ─────────┘                  └────┘               └┘  └─
par  ─────────┘                  └────┘               └┘  └─
pid  ─────────┘                  └─────┘               └┘  └─
st   ────────────────────────────┘└────────────────────┘└─────
288            (by simpa using hε' i),
id                             └─┘ 
src  ─────────┘   └──────────┘    └─
typ  ─────────┘   └──────────┘└─┘└─
doc  ─────────┘   └──────────┘    └─
txt  ─────────┘   └──────────┘    └─
par  ─────────┘   └──────────┘    └─
pid  ─────────┘   └───────────┘    └──
st   ────────────┘└────────────────┘└─
289        simpa [μ, infi_lt_iff] },
id                  └─────────┘
src  ─────┘└─────┘ └┘└─────────┘└┘
typ  ─────┘└─────┘└┘└─────────┘└┘
doc  ─────┘└─────┘ └┘           └┘
txt  ─────┘└─────┘ └┘           └┘
par  ─────┘└─────┘ └┘           └┘
pid  ────────────┘ └┘           └─┘
st   ────────────────────────────┘└┘
290      refine le_trans _ (ennreal.tsum_le_tsum $ λ i, le_of_lt (hf i).2),
id              └──────┘    └──────────────────┘        └──────┘  └┘
src      └─────┘└──────┘└─┘ └──────────────────┘  └──┘└──────┘    └──┘
typ      └─────┘└──────┘└─┘ └──────────────────┘  └──┘└──────┘ └┘ └──┘
doc      └─────┘        └─┘                       └──┘            └──┘
txt      └─────┘        └─┘                       └──┘            └──┘
par      └─────┘        └─┘                       └──┘            └──┘
pid                    └─┘                       └──┘            └──┘
st   ────────────────────────────────────────────────────────────────────┘└─
291      rw [← ennreal.tsum_prod, ← tsum_equiv equiv.nat_prod_nat_equiv_nat.symm],
id             └───────────────┘    └────────┘ └───────────────────────────────┘
src      └────┘└───────────────┘└──┘└────────┘└───────────────────────────────┘
typ      └────┘└───────────────┘└──┘└────────┘└───────────────────────────────┘
doc      └────┘                 └──┘                                           
txt      └────┘                 └──┘                                           
par      └────┘                 └──┘                                           
pid        └──┘                 └──┘                                           
st   ──────────────────────────┘└──────────────────────────────────────────────┘└──
292      swap, {apply_instance},
src      └──┘   └────────────┘
typ      └──┘   └────────────┘
doc      └──┘   └────────────┘
txt      └──┘   └────────────┘
par      └──┘   └────────────┘
st   ───────┘└───────────────┘└┘
293      refine infi_le_of_le _ (infi_le _ _),
id              └───────────┘    └─────┘
src      └─────┘└───────────┘└─┘ └─────┘└───┘
typ      └─────┘└───────────┘└─┘ └─────┘└───┘
doc      └─────┘             └─┘        └───┘
txt      └─────┘             └─┘        └───┘
par      └─────┘             └─┘        └───┘
pid                         └─┘        └───┘
st   ───────────────────────────────────────┘└─
294      exact Union_subset (λ i, subset.trans (hf i).1 $
id                                              └┘
src      └────┘              └──┘                └──┘ 
typ      └────┘              └──┘             └┘ └──┘ 
doc      └────┘              └──┘                └──┘ 
txt      └────┘              └──┘                └──┘ 
par      └────┘              └──┘                └──┘ 
pid                         └──┘                └──┘ 
st   ─────────────────────────────────────────────────────
295        Union_subset $ λ j, subset.trans (by simp) $
id         └──────────┘        └──────────┘
src  ─────┘└──────────┘  └──┘└──────────┘   └──┘└┘ 
typ  ─────┘└──────────┘  └──┘└──────────┘   └──┘└┘ 
doc  ─────┘              └──┘               └──┘└┘ 
txt  ─────┘              └──┘               └──┘└┘ 
par  ─────┘              └──┘               └──┘└┘ 
pid  ─────┘              └──┘               └─────┘ 
st   ─────────────────────────────────────────┘└───┘└───
296        subset_Union _ $ equiv.nat_prod_nat_equiv_nat (i, j)),
id         └──────────┘     └──────────────────────────┘
src  ─────┘└──────────┘└─┘ └──────────────────────────┘  └┘ └┘
typ  ─────┘└──────────┘└─┘ └──────────────────────────┘  └┘ └┘
doc  ─────┘            └─┘                               └┘ └┘
txt  ─────┘            └─┘                               └┘ └┘
par  ─────┘            └─┘                               └┘ └┘
pid  ─────┘            └─┘                               └┘ └┘
st   ──────────────────────────────────────────────────────────┘└─
297    end }
st   ────┘
298  
299  theorem of_function_le {α : Type*} (m : set α → ennreal) (m_empty s) :
id                                           └─┘    └─────┘
src                                          └─┘     └─────┘
typ                                          └─┘    └─────┘
doc                                                  └─────┘
300    outer_measure.of_function m m_empty s ≤ m s :=
id     └───────────────────────┘  └─────┘    
src    └───────────────────────┘             
typ    └───────────────────────┘  └─────┘    
doc    └───────────────────────┘
301  let f : ℕ → set α := λi, nat.rec_on i s (λn s, ∅) in
id             └─┘        └────────┘        
src             └─┘          └────────┘            
typ            └─┘        └────────┘        
302  infi_le_of_le f $ infi_le_of_le (subset_Union f 0) $ le_of_eq $
id   └───────────┘    └───────────┘  └──────────┘       └──────┘
src  └───────────┘     └───────────┘  └──────────┘        └──────┘
typ  └───────────┘    └───────────┘  └──────────┘       └──────┘
303  calc (∑i, m (f i)) = ({0} : finset ℕ).sum (λi, m (f i)) :
id                        └────┘  └─┘         
src                           └────┘  └─┘
typ                       └────┘  └─┘         
doc                            └────┘
304      tsum_eq_sum $ by intro i; cases i; simp [m_empty]
id       └─────────┘                             └─────┘
src      └─────────┘      └─────┘  └────┘   └────┘       └─
typ      └─────────┘      └─────┘  └────┘  └────┘└─────┘└─
doc                       └─────┘  └────┘   └────┘       └─
txt                       └─────┘  └────┘   └────┘       └─
par                       └─────┘  └────┘   └────┘       └─
pid                            └┘                     
st                       └─────────────────────────────────
305    ... = m s : by simp; refl
id            
src  ─┘               └──┘  └────
typ  ─┘             └──┘  └────
doc  ─┘               └──┘  └────
txt  ─┘               └──┘  └────
par  ─┘               └──┘  └────
pid  ─┘                         
st   ─┘              └───────────
306  
src  
typ  
doc  
txt  
par  
pid  
st   
307  theorem le_of_function {α : Type*} {m m_empty} {μ : outer_measure α} :
id                                                       └───────────┘ 
src                                                      └───────────┘
typ                                                      └───────────┘ 
308    μ ≤ outer_measure.of_function m m_empty ↔ ∀ s, μ s ≤ m s :=
id       └───────────────────────┘  └─────┘          
src       └───────────────────────┘                     
typ      └───────────────────────┘  └─────┘          
doc        └───────────────────────┘
309  ⟨λ H s, le_trans (H _) (of_function_le _ _ _),
id         └──────┘       └────────────┘
src          └──────┘        └────────────┘
typ        └──────┘       └────────────┘
310   λ H s, le_infi $ λ f, le_infi $ λ hs,
id         └─────┘       └─────┘     └┘
src          └─────┘        └─────┘
typ        └─────┘       └─────┘     └┘
311    le_trans (μ.mono hs) $ le_trans (μ.Union f) $
id     └──────┘  └───┘ └┘    └──────┘  └────┘ 
src    └──────┘   └───┘       └──────┘   └────┘
typ    └──────┘  └───┘ └┘    └──────┘  └────┘ 
312    ennreal.tsum_le_tsum $ λ i, H _⟩
id     └──────────────────┘       
src    └──────────────────┘
typ    └──────────────────┘       
313  
314  end of_function
315  
316  section caratheodory_measurable
317  universe u
318  parameters {α : Type u} (m : outer_measure α)
id                               └───────────┘
src                               └───────────┘
typ                              └───────────┘
319  include m
320  
321  local attribute [simp] set.inter_comm set.inter_left_comm set.inter_assoc
id                          └────────────┘ └─────────────────┘ └─────────────┘
src                         └────────────┘ └─────────────────┘ └─────────────┘
typ                         └────────────┘ └─────────────────┘ └─────────────┘
doc                   └──┘
322  
323  variables {s s₁ s₂ : set α}
id                        └─┘
src                       └─┘
typ                       └─┘
324  
325  private def C (s : set α) := ∀t, m t = m (t ∩ s) + m (t \ s)
id                      └─┘                       
src                     └─┘                               
typ                     └─┘                       
326  
327  private lemma C_iff_le {s : set α} : C s ↔ ∀t, m (t ∩ s) + m (t \ s) ≤ m t :=
id                               └─┘                          
src                              └─┘                                 
typ                              └─┘                          
328  forall_congr $ λ t, le_antisymm_iff.trans $ and_iff_right $
id   └──────────┘       └─────────────┘└────┘   └───────────┘
src  └──────────┘        └─────────────┘└────┘   └───────────┘
typ  └──────────┘       └─────────────┘└────┘   └───────────┘
329  by convert m.union _ _; rw inter_union_diff t s
id              └─────┘         └──────────────┘  
src     └──────┘└─────┘└──┘  └─┘└──────────────┘  
typ     └──────┘└─────┘└──┘  └─┘└──────────────┘
doc     └──────┘       └──┘  └─┘                  
txt     └──────┘       └──┘  └─┘                  
par     └──────┘       └──┘  └─┘                  
pid                   └──┘                      
st     └───────────────────────┘└──────────────┘└────
330  
src  
typ  
doc  
txt  
par  
pid  
st   
331  @[simp] private lemma C_empty : C ∅ := by simp [C, m.empty, diff_empty]
id                                                            └────────┘
src                                          └────┘└┘       └┘└────────┘└─
typ                                          └────┘└┘└─────┘└┘└────────┘└─
doc    └──┘                                    └────┘ └┘       └┘          └─
txt                                            └────┘ └┘       └┘          └─
par                                            └────┘ └┘       └┘          └─
pid                                                 └┘       └┘          
st                                            └──────────────────────────────
332  
src  
typ  
doc  
txt  
par  
pid  
st   
333  private lemma C_compl : C s₁ → C (- s₁) := by simp [C, diff_eq]
id                            └┘      └┘                └─────┘
src                                             └────┘└┘└─────┘└─
typ                           └┘      └┘        └────┘└┘└─────┘└─
doc                                                └────┘ └┘       └─
txt                                                └────┘ └┘       └─
par                                                └────┘ └┘       └─
pid                                                     └┘       
st                                                └──────────────────
334  
src  
typ  
doc  
txt  
par  
pid  
st   
335  @[simp] private lemma C_compl_iff : C (- s) ↔ C s :=
id                                              
src                                             
typ                                             
doc    └──┘
336  ⟨λ h, by simpa using C_compl m h, C_compl⟩
id                       └─────┘    └─────┘
src           └──────────┘└─────┘    └─────┘
typ          └──────────┘└─────┘  └─────┘
doc           └──────────┘        
txt           └──────────┘        
par           └──────────┘        
pid                └────┘        
st           └──────────────────────┘
337  
338  private lemma C_union (h₁ : C s₁) (h₂ : C s₂) : C (s₁ ∪ s₂) :=
id                                └┘         └┘      └┘  └┘
src                                                     
typ                               └┘         └┘      └┘  └┘
339  λ t, begin
id     
typ    
st        └─────
340    rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)),
id         └┘   └┘    └┘   └┘    └┘   └┘      └┘  └┘
src    └──┘   └┘      └─┘      └─┘          └───
typ    └──┘└┘└┘└┘ └┘└─┘└┘ └┘└─┘└┘   └┘└┘└───
doc    └──┘   └┘       └─┘       └─┘           └───
txt    └──┘   └┘       └─┘       └─┘           └───
par    └──┘   └┘       └─┘       └─┘           └───
pid      └┘   └┘       └─┘       └─┘           └───
st   ─────────┘└───────────┘└───────────┘└──────────────────┘└─
341      inter_diff_assoc _ _ s₁, set.inter_assoc _ _ s₁,
id       └──────────────┘     └┘  └─────────────┘     └┘
src  ───┘└──────────────┘└───┘  └┘└─────────────┘└───┘  └─
typ  ───┘└──────────────┘└───┘└┘└┘└─────────────┘└───┘└┘└─
doc  ───┘                └───┘  └┘               └───┘  └─
txt  ───┘                └───┘  └┘               └───┘  └─
par  ───┘                └───┘  └┘               └───┘  └─
pid  ───┘                └───┘  └┘               └───┘  └─
st   ──────────────────────────┘└──────────────────────┘└─
342      inter_eq_self_of_subset_right (set.subset_union_left _ _),
id       └───────────────────────────┘  └───────────────────┘
src  ───┘└───────────────────────────┘ └───────────────────┘└──────
typ  ───┘└───────────────────────────┘ └───────────────────┘└──────
doc  ───┘                                                   └──────
txt  ───┘                                                   └──────
par  ───┘                                                   └──────
pid  ───┘                                                   └──────
st   ────────────────────────────────────────────────────────────┘└─
343      union_diff_left, h₂ (t ∩ s₁)],
id       └─────────────┘  └┘     └┘
src  ───┘└─────────────┘└┘       └┘
typ  ───┘└─────────────┘└┘└┘  └┘└┘
doc  ───┘               └┘       └┘
txt  ───┘               └┘       └┘
par  ───┘               └┘       └┘
pid  ───┘               └┘       └┘
st   ──────────────────┘└───────────┘└──
344    simp [diff_eq]
id           └─────┘
src    └────┘└─────┘└┘
typ    └────┘└─────┘└┘
doc    └────┘       └┘
txt    └────┘       └┘
par    └────┘       └┘
pid               
st   ────────────────┘
345  end
st   └─┘
346  
347  private lemma measure_inter_union (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : C s₁) {t : set α} :
id                                          └┘  └┘           └┘       └─┘ 
src                                                                   └─┘
typ                                         └┘  └┘           └┘       └─┘ 
348    m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂) :=
id          └┘  └┘        └┘       └┘
src                                     
typ         └┘  └┘        └┘       └┘
349  by rw [h₁, set.inter_assoc, set.union_inter_cancel_left,
id          └┘  └─────────────┘  └─────────────────────────┘
src     └──┘  └┘└─────────────┘└┘└─────────────────────────┘└─
typ     └──┘└┘└┘└─────────────┘└┘└─────────────────────────┘└─
doc     └──┘  └┘               └┘                           └─
txt     └──┘  └┘               └┘                           └─
par     └──┘  └┘               └┘                           └─
pid       └┘  └┘               └┘                           └─
st     └─────┘└───────────────┘└───────────────────────────┘└─
350    inter_diff_assoc, union_diff_cancel_left h]
id     └──────────────┘  └────────────────────┘ 
src  ─┘└──────────────┘└┘└────────────────────┘ └─
typ  ─┘└──────────────┘└┘└────────────────────┘└─
doc  ─┘                └┘                       └─
txt  ─┘                └┘                       └─
par  ─┘                └┘                       └─
pid  ─┘                └┘                       
st   ─────────────────┘└────────────────────────┘
351  
src  
typ  
doc  
txt  
par  
pid  
st   
352  private lemma C_Union_lt {s : ℕ → set α} : ∀{n:ℕ}, (∀i<n, C (s i)) → C (⋃i<n, s i)
id                                    └─┘                             
src                                   └─┘                                  
typ                                   └─┘                             
doc                                                                             
353  | 0       h := by simp [nat.not_lt_zero]
id                           └─────────────┘
src                    └────┘└─────────────┘└┘
typ                    └────┘└─────────────┘└┘
doc                    └────┘               └┘
txt                    └────┘               └┘
par                    └────┘               └┘
pid                                       
st                    └──────────────────────┘
354  | (n + 1) h := by rw Union_lt_succ; exact C_union m
id                       └───────────┘        └─────┘ 
src                   └─┘└───────────┘  └────┘└─────┘ 
typ                   └─┘└───────────┘  └────┘└─────┘
doc                    └─┘               └────┘        
txt                    └─┘               └────┘        
par                    └─┘               └────┘        
pid                                                  
st                    └──────────────────────────────────
355    (h n (le_refl (n + 1)))
id           └─────┘   
src  ─┘    └─────┘  └─────
typ  ─┘    └─────┘ └─────
doc  ─┘              └─────
txt  ─┘              └─────
par  ─┘              └─────
pid  ─┘              └─────
st   ──────────────────────────
356        (C_Union_lt $ assume i hi, h i $ lt_of_lt_of_le hi $ nat.le_succ _)
id          └────────┘                     └────────────┘      └─────────┘
src  ─────┘                  └─────┘   └────────────┘   └─────────┘└───
typ  ─────┘ └────────┘       └─────┘  └────────────┘   └─────────┘└───
doc  ─────┘                  └─────┘                               └───
txt  ─────┘                  └─────┘                               └───
par  ─────┘                  └─────┘                               └───
pid  ─────┘                  └─────┘                               └─┘
st   ──────────────────────────────────────────────────────────────────────────
357  
src  
typ  
doc  
txt  
par  
pid  
st   
358  private lemma C_inter (h₁ : C s₁) (h₂ : C s₂) : C (s₁ ∩ s₂) :=
id                                └┘         └┘      └┘  └┘
src                                                     
typ                               └┘         └┘      └┘  └┘
359  by rw [← C_compl_iff, compl_inter]; from C_union _ (C_compl _ h₁) (C_compl _ h₂)
id            └─────────┘  └─────────┘        └─────┘              └┘   └─────┘   └┘
src     └────┘└─────────┘└┘└─────────┘  └───┘└─────┘└─┘        └─┘  └┘ └─────┘└─┘  └─
typ     └────┘└─────────┘└┘└─────────┘  └───┘└─────┘└─┘        └─┘└┘└┘ └─────┘└─┘└┘└─
doc     └────┘           └┘             └───┘       └─┘        └─┘  └┘        └─┘  └─
txt     └────┘           └┘             └───┘       └─┘        └─┘  └┘        └─┘  └─
par     └────┘           └┘             └───┘       └─┘        └─┘  └┘        └─┘  └─
pid       └──┘           └┘             └───┘       └─┘        └─┘  └┘        └─┘  
st     └────────────────┘└───────────┘└──────────────────────────────────────────────
360  
src  
typ  
doc  
txt  
par  
pid  
st   
361  private lemma C_sum {s : ℕ → set α} (h : ∀i, C (s i)) (hd : pairwise (disjoint on s)) {t : set α} :
id                               └─┘                       └──────┘  └──────┘ └┘         └─┘ 
src                              └─┘                           └──────┘  └──────┘ └┘          └─┘
typ                              └─┘                       └──────┘  └──────┘ └┘         └─┘ 
doc                                                              └──────┘  └──────┘
362    ∀ {n}, (finset.range n).sum (λi, m (t ∩ s i)) = m (t ∩ ⋃i<n, s i)
id           └──────────┘  └─┘                      
src            └──────────┘   └─┘                             
typ          └──────────┘  └─┘                      
doc            └──────────┘                                      
363  | 0            := by simp [nat.not_lt_zero, m.empty]
id                              └─────────────┘
src                       └────┘└─────────────┘└┘       └┘
typ                       └────┘└─────────────┘└┘└─────┘└┘
doc                       └────┘               └┘       └┘
txt                       └────┘               └┘       └┘
par                       └────┘               └┘       └┘
pid                                          └┘       
st                       └───────────────────────────────┘
364  | (nat.succ n) := begin
id      └──────┘
src     └──────┘
typ     └──────┘
st                     └─────
365    simp [Union_lt_succ, range_succ],
id           └───────────┘  └────────┘
src    └────┘└───────────┘└┘└────────┘
typ    └────┘└───────────┘└┘└────────┘
doc    └────┘             └┘          
txt    └────┘             └┘          
par    └────┘             └┘          
pid                     └┘          
st   ─────────────────────────────────┘└─
366    rw [measure_inter_union m _ (h n), C_sum],
id         └─────────────────┘      
src    └──┘└─────────────────┘ └─┘   └─┘     
typ    └──┘└─────────────────┘└─┘ └─┘└───┘
doc    └──┘                    └─┘   └─┘     
txt    └──┘                    └─┘   └─┘     
par    └──┘                    └─┘   └─┘     
pid      └┘                    └─┘   └─┘     
st   ──────────────────────────────────┘└─────┘└──
367    intro a, simpa [range_succ] using λ h₁ i hi h₂, hd _ _ (ne_of_gt hi) ⟨h₁, h₂⟩
id                     └────────┘                      └┘      └──────┘
src    └─────┘  └─────┘└────────┘└──────┘ └───────────┘  └───┘ └──────┘  └┘   └┘  └┘
typ    └─────┘  └─────┘└────────┘└──────┘ └───────────┘└┘└───┘ └──────┘  └┘   └┘  └┘
doc    └─────┘  └─────┘          └──────┘ └───────────┘  └───┘           └┘   └┘  └┘
txt    └─────┘  └─────┘          └──────┘ └───────────┘  └───┘           └┘   └┘  └┘
par    └─────┘  └─────┘          └──────┘ └───────────┘  └───┘           └┘   └┘  └┘
pid         └┘                 └────┘ └───────────┘  └───┘           └┘   └┘  
st   ────────┘└─────────────────────────────────────────────────────────────────────┘
368  end
st   └─┘
369  
370  private lemma C_Union_nat {s : ℕ → set α} (h : ∀i, C (s i))
id                                     └─┘              
src                                    └─┘             
typ                                    └─┘              
371    (hd : pairwise (disjoint on s)) : C (⋃i, s i) :=
id           └──────┘  └──────┘ └┘          
src          └──────┘  └──────┘ └┘          
typ          └──────┘  └──────┘ └┘          
doc          └──────┘  └──────┘              
372  C_iff_le.2 $ λ t, begin
id   └──────┘      
src  └──────┘
typ  └──────┘      
st                     └─────
373    have hp : m (t ∩ ⋃i, s i) ≤ (⨆n, m (t ∩ ⋃i<n, s i)),
id                                           
src    └────────┘       └┘     └┘   └┘
typ    └────────┘       └┘   └┘  └┘
doc    └────────┘        └┘      └┘   └┘
txt    └────────┘        └┘         └┘    └┘
par    └────────┘        └┘         └┘    └┘
pid    └─────┘└─┘        └┘         └┘    └┘
st   ────────────────────────────────────────────────────┘└─
374    { convert m.Union (λ i, t ∩ s i),
id               └─────┘          
src      └──────┘└─────┘  └──┘    
typ      └──────┘└─────┘  └──┘  
doc      └──────┘         └──┘    
txt      └──────┘         └──┘    
par      └──────┘         └──┘    
pid                      └──┘    
st   ───┘└────────────────────────────┘└─
375      { rw inter_Union },
id            └─────────┘
src        └─┘└─────────┘
typ        └─┘└─────────┘
doc        └─┘           
txt        └─┘           
par        └─┘           
pid                     
st   ─────┘└─────────────┘└┘
376      { simp [ennreal.tsum_eq_supr_nat, C_sum m h hd] } },
id               └──────────────────────┘  └───┘   └┘
src        └────┘└──────────────────────┘└┘└───┘    └┘
typ        └────┘└──────────────────────┘└┘└───┘└┘└┘
doc        └────┘                        └┘         └┘
txt        └────┘                        └┘         └┘
par        └────┘                        └┘         └┘
pid                                    └┘         
st   ───────────────────────────────────────────────────┘└──┘
377    refine le_trans (add_le_add_right' hp) _,
id            └──────┘  └───────────────┘ └┘
src    └─────┘└──────┘ └───────────────┘  └─┘
typ    └─────┘└──────┘ └───────────────┘└┘└─┘
doc    └─────┘                            └─┘
txt    └─────┘                            └─┘
par    └─────┘                            └─┘
pid                                      └─┘
st   ─────────────────────────────────────────┘└─
378    rw ennreal.supr_add,
id        └──────────────┘
src    └─┘└──────────────┘
typ    └─┘└──────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────┘└─
379    refine supr_le (λ n, le_trans (add_le_add_left' _)
id            └─────┘       └──────┘  └──────────────┘
src    └─────┘└─────┘  └──┘└──────┘ └──────────────┘└───
typ    └─────┘└─────┘  └──┘└──────┘ └──────────────┘└───
doc    └─────┘         └──┘                         └───
txt    └─────┘         └──┘                         └───
par    └─────┘         └──┘                         └───
pid                   └──┘                         └───
st   ─────────────────────────────────────────────────────
380      (ge_of_eq (C_Union_lt m (λ i _, h i) _))),
id        └──────┘  └────────┘          
src  ───┘ └──────┘ └────────┘   └────┘  └────┘
typ  ───┘ └──────┘ └────────┘  └────┘ └────┘
doc  ───┘                       └────┘  └────┘
txt  ───┘                       └────┘  └────┘
par  ───┘                       └────┘  └────┘
pid  ───┘                       └────┘  └────┘
st   ────────────────────────────────────────────┘└─
381    refine m.mono (diff_subset_diff_right _),
id            └────┘  └────────────────────┘
src    └─────┘└────┘ └────────────────────┘└─┘
typ    └─────┘└────┘ └────────────────────┘└─┘
doc    └─────┘                             └─┘
txt    └─────┘                             └─┘
par    └─────┘                             └─┘
pid                                       └─┘
st   ─────────────────────────────────────────┘└─
382    exact bUnion_subset (λ i _, subset_Union _ i),
id           └───────────┘         └──────────┘
src    └────┘└───────────┘  └────┘└──────────┘└─┘ 
typ    └────┘└───────────┘  └────┘└──────────┘└─┘ 
doc    └────┘               └────┘            └─┘ 
txt    └────┘               └────┘            └─┘ 
par    └────┘               └────┘            └─┘ 
pid                        └────┘            └─┘ 
st   ──────────────────────────────────────────────┘└─
383  end
st   ──┘
384  
385  private lemma f_Union {s : ℕ → set α} (h : ∀i, C (s i))
id                                 └─┘              
src                                └─┘             
typ                                └─┘              
386    (hd : pairwise (disjoint on s)) : m (⋃i, s i) = ∑i, m (s i) :=
id           └──────┘  └──────┘ └┘                 
src          └──────┘  └──────┘ └┘                   
typ          └──────┘  └──────┘ └┘                 
doc          └──────┘  └──────┘                       
387  begin
st   └─────
388    refine le_antisymm (m.Union_nat s) _,
id            └─────────┘  └─────────┘ 
src    └─────┘└─────────┘ └─────────┘ └─┘
typ    └─────┘└─────────┘ └─────────┘└─┘
doc    └─────┘                        └─┘
txt    └─────┘                        └─┘
par    └─────┘                        └─┘
pid                                  └─┘
st   ─────────────────────────────────────┘└─
389    rw ennreal.tsum_eq_supr_nat,
id        └──────────────────────┘
src    └─┘└──────────────────────┘
typ    └─┘└──────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────────────┘└─
390    refine supr_le (λ n, _),
id            └─────┘
src    └─────┘└─────┘  └────┘
typ    └─────┘└─────┘  └────┘
doc    └─────┘         └────┘
txt    └─────┘         └────┘
par    └─────┘         └────┘
pid                   └────┘
st   ────────────────────────┘└─
391    have := @C_sum _ m _ h hd univ n,
id              └───┘       └┘ └──┘ 
src    └──────┘ └───┘└─┘ └─┘   └──┘
typ    └──────┘ └───┘└─┘└─┘└┘└──┘
doc    └──────┘      └─┘ └─┘       
txt    └──────┘      └─┘ └─┘       
par    └──────┘      └─┘ └─┘       
pid    └───┘└─┘      └─┘ └─┘       
st   ─────────────────────────────────┘└─
392    simp at this, simp [this],
id                         └──┘
src    └──────────┘  └────┘    
typ    └──────────┘  └────┘└──┘
doc    └──────────┘  └────┘    
txt    └──────────┘  └────┘    
par    └──────────┘  └────┘    
pid        └─────┘          
st   ─────────────┘└───────────┘└─
393    exact m.mono (bUnion_subset (λ i _, subset_Union _ i)),
id           └────┘  └───────────┘         └──────────┘
src    └────┘└────┘ └───────────┘  └────┘└──────────┘└─┘ └┘
typ    └────┘└────┘ └───────────┘  └────┘└──────────┘└─┘ └┘
doc    └────┘                      └────┘            └─┘ └┘
txt    └────┘                      └────┘            └─┘ └┘
par    └────┘                      └────┘            └─┘ └┘
pid                               └────┘            └─┘ └┘
st   ───────────────────────────────────────────────────────┘└─
394  end
st   ──┘
395  
396  private def caratheodory_dynkin : measurable_space.dynkin_system α :=
id                                     └────────────────────────────┘ 
src                                    └────────────────────────────┘
typ                                    └────────────────────────────┘ 
doc                                    └────────────────────────────┘
397  { has := C,
id            
src           
typ           
398    has_empty := C_empty,
id                  └─────┘
src                 └─────┘
typ                 └─────┘
399    has_compl := assume s, C_compl,
id                           └─────┘
src                           └─────┘
typ                          └─────┘
400    has_Union_nat := assume f hf hn, C_Union_nat hn hf }
id                              └┘ └┘  └─────────┘ └┘ └┘
src                                     └─────────┘
typ                             └┘ └┘  └─────────┘ └┘ └┘
401  
402  /-- Given an outer measure `μ`, the Caratheodory measurable space is
403    defined such that `s` is measurable if `∀t, μ t = μ (t ∩ s) + μ (t \ s)`. -/
404  protected def caratheodory : measurable_space α :=
id                                └──────────────┘ 
src                               └──────────────┘
typ                               └──────────────┘ 
405  caratheodory_dynkin.to_measurable_space $ assume s₁ s₂, C_inter
id   └─────────────────┘└──────────────────┘          └┘ └┘  └─────┘
src  └─────────────────┘└──────────────────┘                 └─────┘
typ  └─────────────────┘└──────────────────┘          └┘ └┘  └─────┘
406  
407  lemma is_caratheodory {s : set α} :
id                              └─┘ 
src                             └─┘
typ                             └─┘ 
408    caratheodory.is_measurable s ↔ ∀t, m t = m (t ∩ s) + m (t \ s) :=
id     └──────────┘└────────────┘                    
src    └──────────┘└────────────┘                            
typ    └──────────┘└────────────┘                    
doc    └──────────┘
409  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
410  
411  lemma is_caratheodory_le {s : set α} :
id                                 └─┘ 
src                                └─┘
typ                                └─┘ 
412    caratheodory.is_measurable s ↔ ∀t, m (t ∩ s) + m (t \ s) ≤ m t :=
id     └──────────┘└────────────┘                     
src    └──────────┘└────────────┘                           
typ    └──────────┘└────────────┘                     
doc    └──────────┘
413  C_iff_le
id   └──────┘
src  └──────┘
typ  └──────┘
414  
415  protected lemma Union_eq_of_caratheodory {s : ℕ → set α}
id                                                    └─┘ 
src                                                   └─┘
typ                                                   └─┘ 
416    (h : ∀i, caratheodory.is_measurable (s i)) (hd : pairwise (disjoint on s)) :
id             └──────────┘└────────────┘            └──────┘  └──────┘ └┘ 
src             └──────────┘└────────────┘              └──────┘  └──────┘ └┘
typ            └──────────┘└────────────┘            └──────┘  └──────┘ └┘ 
doc             └──────────┘                            └──────┘  └──────┘
417    m (⋃i, s i) = ∑i, m (s i) :=
id                
src                
typ               
doc                 
418  f_Union h hd
id   └─────┘  └┘
src  └─────┘
typ  └─────┘  └┘
419  
420  end caratheodory_measurable
421  
422  variables {α : Type*}
423  
424  lemma caratheodory_is_measurable {m : set α → ennreal} {s : set α}
id                                         └─┘    └─────┘       └─┘ 
src                                        └─┘     └─────┘       └─┘
typ                                        └─┘    └─────┘       └─┘ 
doc                                                └─────┘
425    {h₀ : m ∅ = 0} (hs : ∀t, m (t ∩ s) + m (t \ s) ≤ m t) :
id                                         
src                                              
typ                                        
426    (outer_measure.of_function m h₀).caratheodory.is_measurable s :=
id      └───────────────────────┘  └┘ └──────────┘ └───────────┘  
src     └───────────────────────┘      └──────────┘ └───────────┘
typ     └───────────────────────┘  └┘ └──────────┘ └───────────┘  
doc     └───────────────────────┘      └──────────┘
427  let o := (outer_measure.of_function m h₀) in
id            └───────────────────────┘  └┘
src            └───────────────────────┘
typ           └───────────────────────┘  └┘
doc            └───────────────────────┘
428  (is_caratheodory_le o).2 $ λ t,
id    └────────────────┘        
src   └────────────────┘   
typ   └────────────────┘        
429  le_infi $ λ f, le_infi $ λ hf, begin
id   └─────┘       └─────┘     └┘
src  └─────┘        └─────┘
typ  └─────┘       └─────┘     └┘
st                                  └─────
430    refine le_trans (add_le_add'
id            └──────┘  └─────────┘
src    └─────┘└──────┘ └─────────┘
typ    └─────┘└──────┘ └─────────┘
doc    └─────┘                    
txt    └─────┘                    
par    └─────┘                    
pid                              
st   ───────────────────────────────
431      (infi_le_of_le (λi, f i ∩ s) $ infi_le _ _)
id                               
src  ───┘                └─┘   └┘        └─────
typ  ───┘                └─┘   └┘        └─────
doc  ───┘                └─┘    └┘        └─────
txt  ───┘                └─┘    └┘        └─────
par  ───┘                └─┘    └┘        └─────
pid  ───┘                └─┘    └┘        └─────
st   ────────────────────────────────────────────────
432      (infi_le_of_le (λi, f i \ s) $ infi_le _ _)) _,
id        └───────────┘              └─────┘
src  ───┘ └───────────┘  └─┘   └┘ └─────┘└──────┘
typ  ───┘ └───────────┘  └─┘ └┘ └─────┘└──────┘
doc  ───┘                └─┘    └┘        └──────┘
txt  ───┘                └─┘    └┘        └──────┘
par  ───┘                └─┘    └┘        └──────┘
pid  ───┘                └─┘    └┘        └──────┘
st   ─────────────────────────────────────────────────┘└─
433    { rw ← Union_inter,
id            └─────────┘
src      └───┘└─────────┘
typ      └───┘└─────────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ───┘└──────────────┘└─
434      exact inter_subset_inter_left _ hf },
id             └─────────────────────┘   └┘
src      └────┘└─────────────────────┘└─┘  
typ      └────┘└─────────────────────┘└─┘└┘
doc      └────┘                       └─┘  
txt      └────┘                       └─┘  
par      └────┘                       └─┘  
pid                                  └─┘  
st   ──────────────────────────────────────┘└┘
435    { rw ← Union_diff,
id            └────────┘
src      └───┘└────────┘
typ      └───┘└────────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ───┘└─────────────┘└─
436      exact diff_subset_diff_left hf },
id             └───────────────────┘ └┘
src      └────┘└───────────────────┘  
typ      └────┘└───────────────────┘└┘
doc      └────┘                       
txt      └────┘                       
par      └────┘                       
pid                                  
st   ──────────────────────────────────┘└┘
437    { rw ← ennreal.tsum_add,
id            └──────────────┘
src      └───┘└──────────────┘
typ      └───┘└──────────────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ────────────────────────┘└─
438      exact ennreal.tsum_le_tsum (λ i, hs _) }
id             └──────────────────┘       └┘
src      └────┘└──────────────────┘  └──┘  └──┘
typ      └────┘└──────────────────┘  └──┘└┘└──┘
doc      └────┘                      └──┘  └──┘
txt      └────┘                      └──┘  └──┘
par      └────┘                      └──┘  └──┘
pid                                 └──┘  └─┘
st   ──────────────────────────────────────────┘└─
439  end
st   ──┘
440  
441  @[simp] theorem zero_caratheodory : (0 : outer_measure α).caratheodory = ⊤ :=
id                                            └───────────┘  └──────────┘   
src                                           └───────────┘   └──────────┘   
typ                                           └───────────┘  └──────────┘   
doc    └──┘                                                   └──────────┘
442  top_unique $ λ s _ t, (add_zero _).symm
id   └────────┘          └──────┘   └──┘
src  └────────┘             └──────┘   └──┘
typ  └────────┘          └──────┘   └──┘
443  
444  theorem top_caratheodory : (⊤ : outer_measure α).caratheodory = ⊤ :=
id                                  └───────────┘  └──────────┘   
src                                 └───────────┘   └──────────┘   
typ                                 └───────────┘  └──────────┘   
doc                                                  └──────────┘
445  top_unique $ assume s hs, (is_caratheodory_le _).2 $ assume t,
id   └────────┘           └┘   └────────────────┘              
src  └────────┘                 └────────────────┘   
typ  └────────┘           └┘   └────────────────┘              
446    t.eq_empty_or_nonempty.elim (λ ht, by simp [ht])
id     └───────────────────┘└───┘    └┘           └┘
src     └───────────────────┘└───┘           └────┘  
typ    └───────────────────┘└───┘    └┘     └────┘└┘
doc                                          └────┘  
txt                                          └────┘  
par                                          └────┘  
pid                                                
st                                          └────────┘
447      (λ ht, by simp only [ht, top_apply, le_top])
id          └┘                └┘  └───────┘  └────┘
src                └─────────┘  └┘└───────┘└┘└────┘
typ         └┘     └─────────┘└┘└┘└───────┘└┘└────┘
doc                └─────────┘  └┘         └┘      
txt                └─────────┘  └┘         └┘      
par                └─────────┘  └┘         └┘      
pid                    └──┘└┘  └┘         └┘      
st                └────────────────────────────────┘
448  
449  theorem le_add_caratheodory (m₁ m₂ : outer_measure α) :
id                                        └───────────┘ 
src                                       └───────────┘
typ                                       └───────────┘ 
450    m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂ : outer_measure α).caratheodory :=
id     └┘└───────────┘  └┘└───────────┘   └┘  └┘   └───────────┘  └──────────┘
src      └───────────┘    └───────────┘            └───────────┘   └──────────┘
typ    └┘└───────────┘  └┘└───────────┘   └┘  └┘   └───────────┘  └──────────┘
doc      └───────────┘     └───────────┘                              └──────────┘
451  λ s ⟨hs₁, hs₂⟩ t, by simp [hs₁ t, hs₂ t]
id                           └─┘   └─┘ 
src                       └────┘    └┘    └─
typ                    └────┘└─┘└┘└─┘└─
doc                       └────┘    └┘    └─
txt                       └────┘    └┘    └─
par                       └────┘    └┘    └─
pid                               └┘    
st                       └────────────────────
452  
src  
typ  
doc  
txt  
par  
pid  
st   
453  theorem le_sum_caratheodory {ι} (m : ι → outer_measure α) :
id                                           └───────────┘ 
src                                           └───────────┘
typ                                          └───────────┘ 
454    (⨅ i, (m i).caratheodory) ≤ (sum m).caratheodory :=
id           └──────────┘     └─┘  └──────────┘
src             └──────────┘     └─┘   └──────────┘
typ          └──────────┘     └─┘  └──────────┘
doc             └──────────┘            └──────────┘
455  λ s h t, by simp [λ i,
id       
src              └────┘ └───
typ           └────┘ └───
doc              └────┘ └───
txt              └────┘ └───
par              └────┘ └───
pid                   └───
st              └───────────
456    measurable_space.is_measurable_infi.1 h i t, ennreal.tsum_add]
id     └─────────────────────────────────┘        └──────────────┘
src  ─┘└─────────────────────────────────┘└─┘   └┘└──────────────┘└─
typ  ─┘└─────────────────────────────────┘└─┘ └┘└──────────────┘└─
doc  ─┘                                   └─┘   └┘                └─
txt  ─┘                                   └─┘   └┘                └─
par  ─┘                                   └─┘   └┘                └─
pid  ─┘                                   └─┘   └┘                
st   ─────────────────────────────────────────────────────────────────
457  
src  
typ  
doc  
txt  
par  
pid  
st   
458  theorem le_smul_caratheodory (a : ennreal) (m : outer_measure α) :
id                                     └─────┘       └───────────┘ 
src                                    └─────┘       └───────────┘
typ                                    └─────┘       └───────────┘ 
doc                                    └─────┘
459    m.caratheodory ≤ (a • m).caratheodory :=
id     └───────────┘      └──────────┘
src     └───────────┘        └──────────┘
typ    └───────────┘      └──────────┘
doc     └───────────┘          └──────────┘
460  λ s h t, by simp [h t, mul_add]
id                     └─────┘
src              └────┘  └┘└─────┘└─
typ           └────┘└┘└─────┘└─
doc              └────┘  └┘       └─
txt              └────┘  └┘       └─
par              └────┘  └┘       └─
pid                    └┘       
st              └────────────────────
461  
src  
typ  
doc  
txt  
par  
pid  
st   
462  @[simp] theorem dirac_caratheodory (a : α) : (dirac a).caratheodory = ⊤ :=
id                                                └───┘  └──────────┘   
src                                                └───┘   └──────────┘   
typ                                               └───┘  └──────────┘   
doc    └──┘                                        └───┘   └──────────┘
463  top_unique $ λ s _ t, begin
id   └────────┘       
src  └────────┘
typ  └────────┘       
st                         └─────
464    by_cases a ∈ t; simp [h],
id                        
src    └───────┘    └────┘ 
typ    └───────┘  └────┘
doc    └───────┘     └────┘ 
txt    └───────┘     └────┘ 
par    └───────┘     └────┘ 
pid                      
st   ─────────────────────────┘└─
465    by_cases a ∈ s; simp [h]
id                         
src    └───────┘     └────┘ └┘
typ    └───────┘   └────┘└┘
doc    └───────┘     └────┘ └┘
txt    └───────┘     └────┘ └┘
par    └───────┘     └────┘ └┘
pid                      
st   ──────────────────────────┘
466  end
st   └─┘
467  
468  section Inf_gen
469  
470  def Inf_gen (m : set (outer_measure α)) (s : set α) : ennreal :=
id                    └─┘  └───────────┘         └─┘     └─────┘
src                   └─┘  └───────────┘          └─┘      └─────┘
typ                   └─┘  └───────────┘         └─┘     └─────┘
doc                                                        └─────┘
471  ⨆(h : s.nonempty), ⨅ (μ : outer_measure α) (h : μ ∈ m), μ s
id        └───────┘        └───────────┘             
src        └───────┘        └───────────┘              
typ       └───────┘        └───────────┘             
doc        └───────┘                                    
472  
473  @[simp] lemma Inf_gen_empty (m : set (outer_measure α)) : Inf_gen m ∅ = 0 :=
id                                    └─┘  └───────────┘      └─────┘   
src                                   └─┘  └───────────┘       └─────┘    
typ                                   └─┘  └───────────┘      └─────┘   
doc    └──┘
474  by simp [Inf_gen, empty_not_nonempty]
id            └─────┘  └────────────────┘
src     └────┘└─────┘└┘└────────────────┘└─
typ     └────┘└─────┘└┘└────────────────┘└─
doc     └────┘       └┘                  └─
txt     └────┘       └┘                  └─
par     └────┘       └┘                  └─
pid                └┘                  
st     └───────────────────────────────────
475  
src  
typ  
doc  
txt  
par  
pid  
st   
476  lemma Inf_gen_nonempty1 (m : set (outer_measure α)) (t : set α) (h : t.nonempty) :
id                                └─┘  └───────────┘         └─┘        └───────┘
src                               └─┘  └───────────┘          └─┘          └───────┘
typ                               └─┘  └───────────┘         └─┘        └───────┘
doc                                                                        └───────┘
477    Inf_gen m t = (⨅ (μ : outer_measure α) (h : μ ∈ m), μ t) :=
id     └─────┘           └───────────┘             
src    └─────┘             └───────────┘              
typ    └─────┘           └───────────┘             
doc                                                     
478  by rw [Inf_gen, supr_pos h]
id          └─────┘  └──────┘ 
src     └──┘└─────┘└┘└──────┘ └─
typ     └──┘└─────┘└┘└──────┘└─
doc     └──┘       └┘         └─
txt     └──┘       └┘         └─
par     └──┘       └┘         └─
pid       └┘       └┘         
st     └──────────┘└──────────┘
479  
src  
typ  
doc  
txt  
par  
pid  
st   
480  lemma Inf_gen_nonempty2 (m : set (outer_measure α)) (μ) (h : μ ∈ m) (t) :
id                                └─┘  └───────────┘               
src                               └─┘  └───────────┘                
typ                               └─┘  └───────────┘               
481    Inf_gen m t = (⨅ (μ : outer_measure α) (h : μ ∈ m), μ t) :=
id     └─────┘           └───────────┘             
src    └─────┘             └───────────┘              
typ    └─────┘           └───────────┘             
doc                                                     
482  begin
st   └─────
483    cases t.eq_empty_or_nonempty with ht ht,
id           └────────────────────┘
src    └────┘└────────────────────┘└─────────┘
typ    └────┘└────────────────────┘└─────────┘
doc    └────┘                      └─────────┘
txt    └────┘                      └─────────┘
par    └────┘                      └─────────┘
pid                               └─────────┘
st   ────────────────────────────────────────┘└─
484    { simp [ht],
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid            
st   ───┘└───────┘└─
485      refine (bot_unique $ infi_le_of_le μ $ _).symm,
id               └────────┘   └───────────┘ 
src      └─────┘ └────────┘ └───────────┘  └──────┘
typ      └─────┘ └────────┘ └───────────┘ └──────┘
doc      └─────┘                           └──────┘
txt      └─────┘                           └──────┘
par      └─────┘                           └──────┘
pid                                       └─────┘
st   ─────────────────────────────────────────────────┘└─
486      refine infi_le_of_le h (le_refl ⊥) },
id              └───────────┘   └─────┘ 
src      └─────┘└───────────┘  └─────┘└┘
typ      └─────┘└───────────┘ └─────┘└┘
doc      └─────┘                       └┘
txt      └─────┘                       └┘
par      └─────┘                       └┘
pid                                   
st   ──────────────────────────────────────┘└┘
487    { exact Inf_gen_nonempty1 m t ht }
id             └───────────────┘   └┘
src      └────┘└───────────────┘    
typ      └────┘└───────────────┘└┘
doc      └────┘                     
txt      └────┘                     
par      └────┘                     
pid                                
st   ──────────────────────────────────┘└─
488  end
st   ──┘
489  
490  lemma Inf_eq_of_function_Inf_gen (m : set (outer_measure α)) :
id                                         └─┘  └───────────┘ 
src                                        └─┘  └───────────┘
typ                                        └─┘  └───────────┘ 
491    Inf m = outer_measure.of_function (Inf_gen m) (Inf_gen_empty m) :=
id     └─┘   └───────────────────────┘  └─────┘    └───────────┘ 
src    └─┘    └───────────────────────┘  └─────┘     └───────────┘
typ    └─┘   └───────────────────────┘  └─────┘    └───────────┘ 
doc    └─┘     └───────────────────────┘
492  begin
st   └─────
493    refine le_antisymm
id            └─────────┘
src    └─────┘└─────────┘
typ    └─────┘└─────────┘
doc    └─────┘           
txt    └─────┘           
par    └─────┘           
pid                     
st   ─────────────────────
494      (assume t', le_of_function.2 (assume t, _) _)
id                   └────────────┘
src  ───┘       └───┘└────────────┘└─┘       └─────────
typ  ───┘       └───┘└────────────┘└─┘       └─────────
doc  ───┘       └───┘              └─┘       └─────────
txt  ───┘       └───┘              └─┘       └─────────
par  ───┘       └───┘              └─┘       └─────────
pid  ───┘       └───┘              └─┘       └─────────
st   ──────────────────────────────────────────────────
495      (lattice.le_Inf $ assume μ hμ t, le_trans (outer_measure.of_function_le _ _ _) _);
id        └────────────┘                  └──────┘  └──────────────────────────┘
src  ───┘ └────────────┘       └───────┘└──────┘ └──────────────────────────┘└────────┘
typ  ───┘ └────────────┘       └───────┘└──────┘ └──────────────────────────┘└────────┘
doc  ───┘                      └───────┘                                     └────────┘
txt  ───┘                      └───────┘                                     └────────┘
par  ───┘                      └───────┘                                     └────────┘
pid  ───┘                      └───────┘                                     └────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────
496      cases t.eq_empty_or_nonempty with ht ht; simp [ht, Inf_gen_nonempty1],
id             └────────────────────┘                   └┘  └───────────────┘
src      └────┘└────────────────────┘└─────────┘  └────┘  └┘└───────────────┘
typ      └────┘└────────────────────┘└─────────┘  └────┘└┘└┘└───────────────┘
doc      └────┘                      └─────────┘  └────┘  └┘                 
txt      └────┘                      └─────────┘  └────┘  └┘                 
par      └────┘                      └─────────┘  └────┘  └┘                 
pid                                 └─────────┘        └┘                 
st   ────────────────────────────────────────────────────────────────────────┘└─
497    { assume μ hμ, exact (show Inf m ≤ μ, from lattice.Inf_le hμ) t },
id                                └─┘          └────────────┘ └┘  
src      └─────────┘  └────┘     └─┘  └─────┘└────────────┘  └┘ 
typ      └─────────┘  └────┘     └─┘└─────┘└────────────┘└┘└┘
doc      └─────────┘  └────┘     └─┘   └─────┘                └┘ 
txt      └─────────┘  └────┘           └─────┘                └┘ 
par      └─────────┘  └────┘           └─────┘                └┘ 
pid      └─────────┘                  └─────┘                └┘ 
st   ───┘└─────────┘└─────────────────────────────────────────────────┘└┘
498    { exact infi_le_of_le μ (infi_le _ hμ) }
id             └───────────┘   └─────┘   └┘
src      └────┘└───────────┘  └─────┘└─┘  └┘
typ      └────┘└───────────┘ └─────┘└─┘└┘└┘
doc      └────┘                      └─┘  └┘
txt      └────┘                      └─┘  └┘
par      └────┘                      └─┘  └┘
pid                                 └─┘  
st   ────────────────────────────────────────┘└─
499  end
st   ──┘
500  
501  end Inf_gen
502  
503  end outer_measure
504  
505  end measure_theory